\documentclass{llncs}
\usepackage{url}
\usepackage{fullpage}
\usepackage{proof}
\usepackage{amssymb}
\usepackage{latexsym}
\usepackage{xcolor}
\usepackage{mathrsfs}
\usepackage{amsmath}

\newcommand{\frank}[1]{\textcolor{blue}{\textbf{[#1 --Frank]}}}
% My own macros
\newcommand{\m}[3]{ \{#1_1 \mapsto #2_1, ... , #1_n \mapsto #2_n\}#3} 

\begin{document}
%\pagestyle{empty}
\title{Confluence for Lambda Calculus and Its Variants}
\author{Peng Fu}
\institute{Computer Science, The University of Iowa}
\date{March 18, 2013}


\maketitle
\thispagestyle{empty}



\section{Local Lambda-Mu Calculus}

\noindent \textbf{Conventions}: $x,y, z$ will be used as names of variable. $t, a, b$
will be used as names for terms.  
\begin{definition}[Local Lambda Mu Terms]

\

\noindent $t \ :: = \ x \ |  \ \lambda x.t \ | \ t t'  \ | \ \m{x}{t}{t}$

\end{definition}
\noindent \textbf{Notice} : 1. By ``local'', we mean for any $ 1 \leq i \leq n $, $\mathsf{Var}(t_i) \subseteq \{ x_1,..., x_n\}$. 

\noindent 2. We use $\mu$ as a shorthand for $\{x_1 \mapsto t_1,...,x_n \mapsto t_n \}$. So instead of writting $\m{x}{t}{t}$, we write $\mu t $; $\m{x}{t}{\m{y}{b}{t}}$ is now $\mu_1 \mu_2 t$. 

\noindent 3. We use $\bar{\mu}t$ as a shorthand for $\mu_1...\mu_n t$.

\begin{definition}[Substitution]

\

\noindent $[t'/x] x \ : = \  t'$

\

\noindent $[t'/x]y \ := \ y $

\

\noindent $[t'/x]\lambda y.t\ : = \ \lambda y.[t'/x]t$

\

\noindent $[t'/x](t_1 t_2)\ : = \ [t'/x]t_1 [t'/x]t_2$

\

\noindent $[t'/x](\mu t )\ := \mu([t'/x]t)$

\end{definition}

\noindent \textbf{Remarks}: We are working with terms modulo alpha-equivalence. 

\begin{definition}[Beta-Reductions]

\

\noindent \infer{(\lambda x.t)t' \to_{\beta} [t'/x]t}{}

\

\noindent \infer{\mu x_i \to_{\beta} \mu t_i}{(x_i \mapsto t_i) \in \mu}

\

\noindent \infer{\lambda x.t \to_{\beta} \lambda x.t'}{t \to_{\beta}t' }

\

\noindent \infer{t t' \to_{\beta} t'' t'}{t \to_{\beta}t''}

\

\noindent \infer{t t' \to_{\beta} t t''}{t'\to_{\beta}t''}

\

\noindent \infer{\mu t \to_{\beta} \mu t'}{t \to_{\beta}t' }

\end{definition}
\begin{definition}[Mu-Reductions]

\

\noindent \infer{\mu t \to_{\mu} t}{\mathsf{Var}(\mu) \# \mathsf{Var}(t)}

\

\noindent \infer{ \mu(\lambda x.t) \to_{\mu} \lambda x.\mu t}{}

\

\noindent \infer{ \mu(t_1 t_2)  \to_{\mu} (\mu t_1 ) (\mu t_2)}{}

\

\noindent \infer{\lambda x.t \to_{\mu} \lambda x.t'}{t \to_{\mu} t'}

\

\noindent \infer{t t' \to_{\mu} t t''}{t'\to_{\mu} t''}

\

\noindent \infer{t t' \to_{\mu} t'' t'}{t \to_{\mu} t''}

\

\noindent \infer{\mu t \to_{\mu} \mu t'}{t \to_{\mu}t' }


\end{definition}


\section{Confluence}

\noindent We are going to use the following method to conclude the confluence of $\to_{\beta} \cup \to_{\mu}$. 

\begin{lemma}[Interpretation lemma]
Let $\mathcal{R} = \mathcal{R}_1 \cup \mathcal{R}_2$ be the union of two relations, 
$\mathcal{R}_1$ being confluent and strongly normalizing. We denote by $\mathcal{R}_1(a)$ the $\mathcal{R}_1$-noraml form of $a$. Suppose that there is some relation $\mathcal{R}'$ on $\mathcal{R}_1$ normal forms satisfying:

\

$\mathcal{R}' \subseteq \mathcal{R}^*$ and $a \stackrel{\mathcal{R}_2}{\to} b $ implies $ \mathcal{R}_1(a)  \stackrel{\mathcal{R}'^*}{\to}   \mathcal{R}_1(b)$

\

\noindent Then $\mathcal{R}'$ is confluent iff $\mathcal{R}$ is confluent.
  
\end{lemma}

\begin{lemma}
  $\to_{\mu}$ is terminating.
\end{lemma}

\begin{lemma}
  $\to_{\mu}$ is confluent.
\end{lemma}
\begin{proof}
Since $\to_{\mu}$ is terminating, local confluent of $\to_{\mu}$ is enough to conclude confluent.

\end{proof}

\begin{definition}[$\mu$-Normal Forms]
  
\

\noindent $n \ :: = \ x \ | \   \{x_1 \mapsto t_1, ..., x_n \mapsto t_n\}x_i \ | \ \lambda x.n \ | \ n n'$

\end{definition}

\noindent  We can also define the $\mu$ normalization function: $m(t)$ as below.

\begin{definition}

\

\noindent $ m(x) \ : = \  x$

\

\noindent $m(\lambda y.t)\ : = \ \lambda y.m(t)$

\

\noindent $m(t_1 t_2)\ : = \ m(t_1) m(t_2)$

\

\noindent $ m(\bar{\mu}y) \ := y$ if $y \notin \mathsf{Var}(\bar{\mu})$.

\

\noindent $ m(\bar{\mu}y) \ := \mu_i y$ if $y \in \mathsf{Var}(\mu_i)$.

%\noindent $m(\mu \bar{x} = \bar{t}.t) \ := m(t)$ if $\{ x_1,..., x_n\} \# FV(t)$.
\

\noindent $m(\bar{\mu}(t t')) \ :=  m(\bar{\mu} t) m( \bar{\mu}t')$

\

\noindent $m(\bar{\mu}( \lambda x.t)) \ := \lambda x.  m(\bar{\mu}t)$.

\


%% \noindent $m(\{x_1:= t_1, ..., x_i = t_i\} t) \ := \{x_1:= m(t_1), ..., x_i = m(t_i)\} m(t)$

\end{definition}

\begin{definition}[$\beta$ Reduction on $\mu$-normal Forms]

\
  
\infer{n \to_{\beta \mu} m(t)}{n \to_{\beta}t}

\end{definition}

\noindent \textbf{Notice}: From this definition we can conclude: 

\

\infer{\lambda x.n \to_{\beta \mu} \lambda x.n'}{n \to_{\beta \mu} n' }

\

\noindent since $n \to_{\beta} t$ implies $\lambda x.n \to_{\beta} \lambda x.t$. And $m(\lambda x.t) \equiv \lambda x.m(t)$. 

\

\noindent Similarly, the following judgements also hold:

\

\infer{n n' \to_{\beta \mu} n n''}{n' \to_{\beta \mu} n'' }

\

\infer{n n' \to_{\beta \mu} n'' n'}{n \to_{\beta \mu} n'' }


\begin{definition}[Parallelization]

\

\noindent \infer{ n \Rightarrow_{\beta \mu} n}{}

\

\noindent \infer{\mu x_i \Rightarrow_{\beta\mu} m(\mu t_i)}{(x_i \mapsto t_i) \in \mathsf{Var}(\mu)}

\

\noindent \infer{(\lambda x.n_1) n_2 \Rightarrow_{\beta\mu} m([n_1'/x]n_2')}{  n_1\Rightarrow_{\beta\mu} n_1' & n_2\Rightarrow_{\beta\mu} n_2'}

\


\noindent \infer{\lambda x.n \Rightarrow_{\beta\mu} \lambda x.n'}{n \Rightarrow_{\beta\mu}n' }

\

\noindent \infer{n n' \Rightarrow_{\beta\mu} n'' n'''}{n' \Rightarrow_{\beta\mu} n''' & n \Rightarrow_{\beta\mu}n'' }


\end{definition}

\subsection{Lemmas}

\begin{lemma}
  $\to_{\beta\mu} \subseteq \Rightarrow_{\beta\mu} \subseteq \to_{\beta\mu}^*$.
\end{lemma}

\begin{lemma}
If $n_2 \Rightarrow_{\beta\mu} n_2'$, then $m([n_2/x]n_1) \Rightarrow_{\beta\mu} m([n_2'/x]n_1)$.
\end{lemma}

\begin{proof}
\noindent  By induction on the structure of $n_1$. We list a few non-trivial cases:

\

\noindent \textbf{Base Case}: $n_1= x, \m{x}{t}{x_i}$. Obvious. 

\

\noindent \textbf{Step Case}: $n_1= \lambda y.n$. We have $m(\lambda y.[n_2/x]n) \equiv \lambda y.m([n_2/x]n) \stackrel{IH}{\Rightarrow_{\beta\mu}} \lambda y.m([n_2'/x]n) \equiv m(\lambda y.[n_2'/x]n)$.

\

\noindent \textbf{Step Case}: $n_1= n n'$. We have $m([n_2/x]n [n_2/x]n') \equiv m([n_2/x]n) m([n_2/x]n')\stackrel{IH}{\Rightarrow_{\beta\mu}} m([n_2'/x]n) m([n_2'/x]n')\equiv m([n_2'/x]n[n_2'/x]n)$.


\end{proof}

\begin{lemma}
\label{key}
If $n_1 \Rightarrow_{\beta\mu} n_1'$ and $ n_2 \Rightarrow_{\beta\mu} n_2'$, then $m([n_2/x]n_1) \Rightarrow_{\beta\mu} m([n_2'/x]n_1')$.
\end{lemma}

\begin{proof}

\noindent We prove this by induction on the derivation of $n_1 \Rightarrow_{\beta\mu} n_1'$.
  
\

\noindent \textbf{Base Case:}

\

\noindent \infer{n \Rightarrow_{\beta \mu} n}{}

\

\noindent By the lemma above.

\

\noindent \textbf{Base Case:}

\

\noindent \infer{\m{x}{t}{x_i}\Rightarrow_{\beta\mu} m(\m{x}{t}{t_i})}{}

\

\noindent Obvious. 

\

\noindent \textbf{Step Case:}

\

\noindent \infer{(\lambda x.n_1) n_2 \Rightarrow_{\beta\mu} m([n_1'/x]n_2')}{ n_1\Rightarrow_{\beta\mu} n_1' & n_2\Rightarrow_{\beta\mu} n_2'}

\

\noindent We have $m((\lambda x.[n_3/y]n_1) [n_3/y] n_2) \equiv (\lambda x.m([n_3/y]n_1)) m([n_3/y] n_2)$

$ \stackrel{IH}{\Rightarrow_{\beta\mu}} m([m([n_3'/y] n_2')/x]m([n_3'/y] n_1')) \equiv m([n_3'/y]([n_2'/x]n_1'))$.

\

\noindent \textbf{Step Case:}

\

\noindent \infer{ \lambda x.n \Rightarrow_{\beta\mu} \lambda x.n'}{ n \Rightarrow_{\beta\mu}n' }

\

\noindent We have $ m(\lambda x.[n_2/y]n) \equiv \lambda x.m([n_2/y]n) \stackrel{IH}{\Rightarrow_{\beta\mu}} \lambda x.m([n_2'/y]n') \equiv m(\lambda x.[n_2'/y]n') $

\

\noindent \textbf{Step Case:}

\

\noindent \infer{n_1 n_2 \Rightarrow_{\beta\mu} n_1'n_2'}{ n_1\Rightarrow_{\beta\mu} n_1' & n_2\Rightarrow_{\beta\mu} n_2'}

\

\noindent We have $m([n_3/y]n_1 [n_3/y] n_2) \equiv m([n_3/y]n_1) m([n_3/y] n_2)$

$ \stackrel{IH}{\Rightarrow_{\beta\mu}} m([n_3'/y] n_1') m([n_3'/y] n_2')\equiv m([n_3'/y](n_1'n_2'))$.


\end{proof}
\begin{lemma}
  If $ n \Rightarrow_{\beta\mu} n'$ and $ n \Rightarrow_{\beta\mu} n''$, then there exist $n'''$ such that $ n'' \Rightarrow_{\beta\mu} n'''$ and $ n' \Rightarrow_{\beta\mu} n'''$.
\end{lemma}

\begin{proof}
  \noindent By induction on the derivation of $ n \Rightarrow_{\beta\mu} n'$. 

\noindent \textbf{Base Case:}

\

\noindent \infer{ n \Rightarrow_{\beta \mu} n}{}

\

\noindent Obvious.

\

\noindent \textbf{Base Case:}

\

\noindent \infer{ \m{x} {t}{x_i}\Rightarrow_{\beta\mu} m(\m{x}{t}{t_i})}{}

\

\noindent Obvious. 

\

\noindent \textbf{Step Case:}

\

\noindent \infer{(\lambda x.n_1) n_2 \Rightarrow_{\beta\mu} m([n_1'/x]n_2')}{ n_1\Rightarrow_{\beta\mu} n_1' &n_2\Rightarrow_{\beta\mu} n_2'}

\

\noindent If $(\lambda x.n_1) n_2 \Rightarrow_{\beta\mu}(\lambda x.n_1'') n_2''$, where $n_1 \Rightarrow_{\beta\mu}n_1''$ and $n_2 \Rightarrow_{\beta\mu} n_2''$. By lemma \ref{key} and IH, we have $m([n_1'/x]n_2') \Rightarrow_{\beta\mu} m([n_1'''/x]n_2''')$. We also have $ (\lambda x.n_1'') n_2''\Rightarrow_{\beta\mu} m([n_1'''/x]n_2''')$, where  $n_1'' \Rightarrow_{\beta\mu}n_1'''$ and $n_1' \Rightarrow_{\beta\mu}n_1'''$ and $n_2' \Rightarrow_{\beta\mu} n_2'''$ and $n_2' \Rightarrow_{\beta\mu}n_2'''$ .

If $ (\lambda x.n_1) n_2 \Rightarrow_{\beta\mu}m([n_2''/x]n_1'') $, where $n_1 \Rightarrow_{\beta\mu}n_1''$ and $ n_2 \Rightarrow_{\beta\mu} n_2''$. By lemma \ref{key} and IH, we have $ m([n_1'/x]n_2') \Rightarrow_{\beta\mu} m([n_1'''/x]n_2''')$ and $m([n_1''/x]n_2'') \Rightarrow_{\beta\mu} m([n_1'''/x]n_2''')$.

\

\noindent The other cases are either similar to the one above or easy.

\end{proof}

\begin{lemma}
    \label{sub}
    $m(\bar{\mu} ([t_2/x]t_1)) \equiv m( [\bar{\mu} t_2/x]\bar{\mu} t_1)$
\end{lemma}

\begin{proof}
By induction on $t_1$. 
\end{proof}
\begin{lemma}
If $a \to_{\beta} b$, then $ m(a)\to_{\beta\mu}^* m(b)$.
\end{lemma}

\begin{proof}
\noindent   We prove this by induction on the derivation of $a \to_{\beta} b$. We list a few non-trial cases:

\

\noindent \textbf{Base Case:}

\

\noindent \infer{\mu x_i \to_{\beta} \mu t_i}{(x_i \mapsto t_i) \in \mu}

\

\noindent We have $m(\mu x_i) \equiv \mu x_i \to_{\beta\mu} m(\mu  t_i)$ where $ \mu x_i \to_{\beta} \mu  t_i$. 

\

\noindent \textbf{Base Case:}

\

\noindent \infer{(\lambda x.t)t' \to_{\beta} [t'/x]t}{}

\

\noindent We have $ m((\lambda x.t)t') \equiv (\lambda x.m(t))m(t') \to_{\beta\mu} m([m(t)/x]m(t')) \equiv m([t'/x]t)$.

\

\noindent \textbf{Step Case:}

\

\noindent \infer{\lambda x.t \to_{\beta} \lambda x.t'}{t \to_{\beta}t' }

\

\noindent By IH, we have $ m(\lambda x.t)  \equiv  \lambda x.m(t)  \to_{\beta\mu}^* \lambda x.m(t') \equiv m(\lambda x.t') $. 

\

\noindent \textbf{Step Case:}

\

\noindent \infer{\mu t \to_{\beta} \mu t'}{t \to_{\beta}t' }

\

\noindent We want to show $ m(\m{x}{t}{t}) \to_{\beta\mu}  m(\m{x}{t}{t'}) $. If $\{x_1,...,x_n\}\# FV(t)$, then $ m(\m{x}{t}{t}) \equiv m(t) \stackrel{IH}{\to_{\beta\mu}}^*  m(t') \equiv m(\m{x}{t}{t'}) $. 

\

\noindent If $\{x_1,...,x_n\}\cap FV(t) \not = \emptyset$, then we do case analysis on the form of $t$. 

%\noindent $t \not = \m{y}{t'}{\bar{\mu}.y_i}$ since it will violate our assumption. 
\

\textbf{Case.} $t=x_i$, this case will not arise.

\

\textbf{Case.} $t = \lambda y.t_1$, then it must be that $t' = \lambda y.t_1'$ where $t_1 \to_{\beta} t_1'$. So 
we get $ \mu t_1 \to_{\beta} \mu t_1'$. By IH, we have $ m(\mu t_1) \to_{\beta\mu}^* m(\mu t_1')$. Thus $ m(\mu(\lambda y.t_1)) \equiv \lambda y.m(\mu t_1) \to_{\beta\mu}^* \lambda y.m(\mu t_1') \equiv m(\mu (\lambda y.t_1'))$. 

\

\textbf{Case.} $t = t_1 t_2$ and $t' = t_1' t_2$, where $t_1 \to_{\beta} t_1'$. We have  $\mu t_1 \to_{\beta } \mu t_1'$. By IH,
$m(\mu t_1) \to_{\beta \mu}^* m(\mu t_1')$. Thus $m(\mu(t_1 t_2)) \equiv m(\mu t_1) m(\mu t_2) \to_{\beta \mu}^* m(\mu t_1') m(\mu t_2) \equiv m(\mu(t_1' t_2))$.
For $t' = t_1 t_2'$, where $t_2 \to_{\beta} t_2'$, we can argue similarly. 

\
 

\textbf{Case.} $t = (\lambda y.t_1)t_2$ and $t' = [t_2/y]t_1$. $m(\mu ((\lambda y.t_1)t_2)) \equiv (\lambda y.m(\mu t_1)))m(\mu t_2)  \to_{\beta\mu} m( [m(\mu t_2)/y] m(\mu t_1)) \equiv m([\mu t_2/y] \mu t_1) \equiv m(\mu [t_2/y]t_1)$(lemma \ref{sub}).

 \

 \textbf{Case.} $t = \mu_1 t_1$, then $t' = \mu_1 t_1'$ where $ t_1 \to_{\beta} t_1'$. We want to show $m(\mu \mu_1 t_1) \to_{\beta\mu}  m(\mu \mu_1 t_1') $. Now we again do a case analysis on $t_1'$, we repeat this process, since $t$ is a finite term, we eventually will only need to show $ m(\mu \mu_1 ....\mu_n t_n) \to_{\beta\mu}  m(\mu \mu_1....\mu_n t_n')$, where $t_n$ is not of the form $\mu t$. Thus we can use the argument similar to last three cases to finish our proof.  

\end{proof}

\begin{theorem}
  $\to_{\beta} \cup \to_{\mu}$ is confluent. 
\end{theorem}


\end{document}
